let n be Element of NAT ; :: thesis: 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); :: thesis: 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 & i + 1 <= len (Gauge C,n) ) and
A2: (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)) & N-min C in cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i,((width (Gauge C,n)) -' 1) ) by JORDAN9:def 1;
A3: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
i + 0 <= i + 1 by XREAL_1:8;
then A4: i <= len (Gauge C,n) by A1, XXREAL_0:2;
4 <= len (Gauge C,n) by JORDAN8:13;
then 1 <= len (Gauge C,n) by XXREAL_0:2;
then A5: [i,(len (Gauge C,n))] in Indices (Gauge C,n) by A1, A3, A4, MATRIX_1:37;
A6: 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 A2, A3, A5, 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 A6, XCMPLX_1:88
.= (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) ; :: thesis: verum