let n be Nat; 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); 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); 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; ( 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 that
A1:
p in BDD C
and
A2:
I = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/]
; ( 1 < I & I + 1 <= width (Gauge (C,n)) )
A3:
(N-bound C) - (S-bound C) > 0
by SPRECT_1:32, XREAL_1:50;
set K = [\((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/];
((((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 6;
then A4:
(((((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:6;
A5:
S-bound C <= S-bound (BDD C)
by A1, Th8;
BDD C is bounded
by JORDAN2C:106;
then
p `2 >= S-bound (BDD C)
by A1, Th5;
then
p `2 >= S-bound C
by A5, XXREAL_0:2;
then
(p `2) - (S-bound C) >= 0
by XREAL_1:48;
then
((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 1 >= 0 + 1
by A3, XREAL_1:6;
then
1 < [\((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/] + 2
by A4, XXREAL_0:2;
hence
1 < I
by A2, INT_1:28; I + 1 <= width (Gauge (C,n))
A6:
len (Gauge (C,n)) = width (Gauge (C,n))
by JORDAN8:def 1;
A7:
N-bound C >= N-bound (BDD C)
by A1, Th9;
BDD C is bounded
by JORDAN2C:106;
then
p `2 <= N-bound (BDD C)
by A1, Th5;
then
p `2 <= N-bound C
by A7, XXREAL_0:2;
then
(p `2) - (S-bound C) <= (N-bound C) - (S-bound C)
by XREAL_1:9;
then
((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C)) <= 1
by A3, XREAL_1:185;
then
(((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n) <= 1 * (2 |^ n)
by XREAL_1:64;
then A8:
((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 3 <= (2 |^ n) + 3
by XREAL_1:7;
I <= ((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2
by A2, INT_1:def 6;
then A9:
I + 1 <= (((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2) + 1
by XREAL_1:6;
len (Gauge (C,n)) = (2 |^ n) + 3
by JORDAN8:def 1;
hence
I + 1 <= width (Gauge (C,n))
by A6, A8, A9, XXREAL_0:2; verum