let n be Element of NAT ; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound (L~ (Cage C,n)) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); N-bound (L~ (Cage C,n)) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))
set a = N-bound C;
set s = S-bound C;
set w = W-bound C;
set f = Cage C,n;
set G = Gauge C,n;
consider i being Element of NAT such that
A1:
1 <= i
and
A2:
i + 1 <= len (Gauge C,n)
and
A3:
(Cage C,n) /. 1 = (Gauge C,n) * i,(width (Gauge C,n))
and
(Cage C,n) /. 2 = (Gauge C,n) * (i + 1),(width (Gauge C,n))
and
N-min C in cell (Gauge C,n),i,((width (Gauge C,n)) -' 1)
and
N-min C <> (Gauge C,n) * i,((width (Gauge C,n)) -' 1)
by JORDAN9:def 1;
A4:
len (Gauge C,n) = width (Gauge C,n)
by JORDAN8:def 1;
4 <= len (Gauge C,n)
by JORDAN8:13;
then A5:
1 <= len (Gauge C,n)
by XXREAL_0:2;
i + 0 <= i + 1
by XREAL_1:8;
then
i <= len (Gauge C,n)
by A2, XXREAL_0:2;
then A6:
[i,(len (Gauge C,n))] in Indices (Gauge C,n)
by A1, A4, A5, MATRIX_1:37;
A7:
2 |^ n <> 0
by NEWTON:102;
thus N-bound (L~ (Cage C,n)) =
(N-min (L~ (Cage C,n))) `2
by EUCLID:56
.=
((Cage C,n) /. 1) `2
by JORDAN9:34
.=
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge C,n)) - 2)))]| `2
by A3, A4, A6, JORDAN8:def 1
.=
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge C,n)) - 2))
by EUCLID:56
.=
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((2 |^ n) + 3) - 2))
by JORDAN8:def 1
.=
((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (2 |^ n))) + (((N-bound C) - (S-bound C)) / (2 |^ n))
.=
((S-bound C) + ((N-bound C) - (S-bound C))) + (((N-bound C) - (S-bound C)) / (2 |^ n))
by A7, XCMPLX_1:88
.=
(N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))
; verum