let i, m be Nat; :: thesis: for x being Real st 2 <= m holds
(x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2)
let x be Real; :: thesis: ( 2 <= m implies (x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2) )
assume 2 <= m ; :: thesis: (x / (2 |^ i)) * (m - 2) = (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2)
then A1: (2 * m) - 2 >= 0 by Lm5;
thus (x / (2 |^ i)) * (m - 2) = x / ((2 |^ i) / (m - 2)) by XCMPLX_1:81
.= x / (((2 |^ i) * 2) / ((m - 2) * 2)) by XCMPLX_1:91
.= (x / ((2 |^ i) * 2)) * ((m - 2) * 2) by XCMPLX_1:81
.= (x / (2 |^ (i + 1))) * (((2 * m) - 2) - 2) by NEWTON:6
.= (x / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2) by A1, XREAL_0:def 2 ; :: thesis: verum