let n be Element of NAT ; :: thesis: for D being non empty Subset of (TOP-REAL 2)
for w being real number 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 number st n > 0 holds
(w / (2 |^ n)) * ((Center (Gauge D,n)) - 2) = w / 2
let w be real number ; :: 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:102;
assume A2: n > 0 ; :: thesis: (w / (2 |^ n)) * ((Center (Gauge D,n)) - 2) = w / 2
then A3: (2 |^ n) mod 2 = 0 by PEPIN:37;
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:69
.= w / 2 by A1, XCMPLX_1:99 ; :: thesis: verum