let n be Element of NAT ; :: thesis: for p being Point of (TOP-REAL 2)
for C being compact non horizontal Subset of (TOP-REAL 2)
for J being Integer st p in BDD C & J = [\(((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
( 1 < J & J + 1 <= width (Gauge C,n) )
let p be Point of (TOP-REAL 2); :: thesis: for C being compact non horizontal Subset of (TOP-REAL 2)
for J being Integer st p in BDD C & J = [\(((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
( 1 < J & J + 1 <= width (Gauge C,n) )
let C be compact non horizontal Subset of (TOP-REAL 2); :: thesis: for J being Integer st p in BDD C & J = [\(((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
( 1 < J & J + 1 <= width (Gauge C,n) )
set W = S-bound C;
set E = N-bound C;
set EW = (N-bound C) - (S-bound C);
set pW = (p `2 ) - (S-bound C);
let I be Integer; :: thesis: ( p in BDD C & I = [\(((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] implies ( 1 < I & I + 1 <= width (Gauge C,n) ) )
assume A1: ( p in BDD C & I = [\(((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] ) ; :: thesis: ( 1 < I & I + 1 <= width (Gauge C,n) )
A2: ( len (Gauge C,n) = (2 |^ n) + 3 & len (Gauge C,n) = width (Gauge C,n) ) by JORDAN8:def 1;
A3: (N-bound C) - (S-bound C) > 0 by SPRECT_1:34, XREAL_1:52;
A4: ( N-bound C >= N-bound (BDD C) & S-bound C <= S-bound (BDD C) ) by A1, Th20, Th21;
set K = [\((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/];
BDD C is Bounded by JORDAN2C:114;
then p `2 >= S-bound (BDD C) by A1, Th6;
then p `2 >= S-bound C by A4, XXREAL_0:2;
then (p `2 ) - (S-bound C) >= 0 by XREAL_1:50;
then A5: ((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 1 >= 0 + 1 by A3, XREAL_1:8;
((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) - 1 < [\((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/] by INT_1:def 4;
then (((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) - 1) + 2 < [\((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/] + 2 by XREAL_1:8;
then 1 < [\((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/] + 2 by A5, XXREAL_0:2;
hence 1 < I by A1, INT_1:51; :: thesis: I + 1 <= width (Gauge C,n)
BDD C is Bounded by JORDAN2C:114;
then p `2 <= N-bound (BDD C) by A1, Th6;
then p `2 <= N-bound C by A4, XXREAL_0:2;
then (p `2 ) - (S-bound C) <= (N-bound C) - (S-bound C) by XREAL_1:11;
then ((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C)) <= 1 by A3, XREAL_1:187;
then (((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n) <= 1 * (2 |^ n) by XREAL_1:66;
then A6: ((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 3 <= (2 |^ n) + 3 by XREAL_1:9;
I <= ((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2 by A1, INT_1:def 4;
then I + 1 <= (((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2) + 1 by XREAL_1:8;
hence I + 1 <= width (Gauge C,n) by A2, A6, XXREAL_0:2; :: thesis: verum