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);
per cases ( n = 0 or n > 0 ) ;
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;
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;
end;