let n be Nat; :: thesis: for D being non empty Subset of (TOP-REAL 2)
for w being Real st n > 0 holds
(w / (2 |^ n)) * ((Center (Gauge (D,n))) - 2) = w / 2
let D be non empty Subset of (TOP-REAL 2); :: thesis: for w being Real st n > 0 holds
(w / (2 |^ n)) * ((Center (Gauge (D,n))) - 2) = w / 2
let w be Real; :: thesis: ( n > 0 implies (w / (2 |^ n)) * ((Center (Gauge (D,n))) - 2) = w / 2 )
set G = Gauge (D,n);
A1: 2 |^ n <> 0 by NEWTON:83;
assume A2: n > 0 ; :: thesis: (w / (2 |^ n)) * ((Center (Gauge (D,n))) - 2) = w / 2
then A3: (2 |^ n) mod 2 = 0 by PEPIN:36;
thus (w / (2 |^ n)) * ((Center (Gauge (D,n))) - 2) = (w / (2 |^ n)) * (((((2 |^ n) + 3) div 2) + 1) - 2) by JORDAN8:def 1
.= (w / (2 |^ n)) * ((((2 |^ n) + 3) div 2) + (1 - 2))
.= (w / (2 |^ n)) * ((((2 |^ n) div 2) + 1) + (- 1)) by A3, Lm1, NAT_D:19
.= (w / (2 |^ n)) * ((2 |^ n) / 2) by A2, PEPIN:64
.= w / 2 by A1, XCMPLX_1:98 ; :: thesis: verum