let E be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat holds Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2

let n be Nat; :: thesis: Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2

reconsider n = n as Nat ;

set G = Gauge (E,n);

let n be Nat; :: thesis: Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2

reconsider n = n as Nat ;

set G = Gauge (E,n);

per cases
( n = 0 or n > 0 )
;

end;

suppose A1:
n = 0
; :: thesis: Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2

A2:
4 = (2 * 2) + 0
;

A3: 0 - 1 < 0 ;

Center (Gauge (E,n)) = ((len (Gauge (E,n))) div 2) + 1 by JORDAN1A:def 1;

then Center (Gauge (E,n)) = (((2 |^ 0) + 3) div 2) + 1 by A1, JORDAN8:def 1

.= ((1 + 3) div 2) + 1 by NEWTON:4

.= (1 + 1) + 1 by A2, NAT_D:def 1

.= ((2 |^ 0) + 1) + 1 by NEWTON:4

.= ((2 |^ (0 -' 1)) + 1) + 1 by A3, XREAL_0:def 2

.= (2 |^ (n -' 1)) + 2 by A1 ;

hence Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2 ; :: thesis: verum

end;A3: 0 - 1 < 0 ;

Center (Gauge (E,n)) = ((len (Gauge (E,n))) div 2) + 1 by JORDAN1A:def 1;

then Center (Gauge (E,n)) = (((2 |^ 0) + 3) div 2) + 1 by A1, JORDAN8:def 1

.= ((1 + 3) div 2) + 1 by NEWTON:4

.= (1 + 1) + 1 by A2, NAT_D:def 1

.= ((2 |^ 0) + 1) + 1 by NEWTON:4

.= ((2 |^ (0 -' 1)) + 1) + 1 by A3, XREAL_0:def 2

.= (2 |^ (n -' 1)) + 2 by A1 ;

hence Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2 ; :: thesis: verum

suppose A4:
n > 0
; :: thesis: Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2

then A5:
0 + 1 <= n
by NAT_1:13;

A6: (2 |^ n) div 2 = (2 |^ n) / 2 by A4, PEPIN:64

.= (2 |^ n) / (2 |^ 1)

.= 2 |^ (n -' 1) by A5, TOPREAL6:10 ;

3 = (2 * 1) + 1 ;

then A7: 3 div 2 = 1 by NAT_D:def 1;

A8: (2 |^ n) mod 2 = 0 by A4, PEPIN:36;

((len (Gauge (E,n))) div 2) + 1 = (((2 |^ n) + 3) div 2) + 1 by JORDAN8:def 1

.= (((2 |^ n) div 2) + (3 div 2)) + 1 by A8, NAT_D:19

.= ((2 |^ n) div 2) + (1 + 1) by A7 ;

hence Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2 by A6, JORDAN1A:def 1; :: thesis: verum

end;A6: (2 |^ n) div 2 = (2 |^ n) / 2 by A4, PEPIN:64

.= (2 |^ n) / (2 |^ 1)

.= 2 |^ (n -' 1) by A5, TOPREAL6:10 ;

3 = (2 * 1) + 1 ;

then A7: 3 div 2 = 1 by NAT_D:def 1;

A8: (2 |^ n) mod 2 = 0 by A4, PEPIN:36;

((len (Gauge (E,n))) div 2) + 1 = (((2 |^ n) + 3) div 2) + 1 by JORDAN8:def 1

.= (((2 |^ n) div 2) + (3 div 2)) + 1 by A8, NAT_D:19

.= ((2 |^ n) div 2) + (1 + 1) by A7 ;

hence Center (Gauge (E,n)) = (2 |^ (n -' 1)) + 2 by A6, JORDAN1A:def 1; :: thesis: verum