let m, i, n be Nat; :: thesis: ( 1 <= i implies [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT )
set i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/];
(((i - 2) / (2 |^ (n -' m))) + 2) - 1 = ((i - 2) / (2 |^ (n -' m))) + (2 - 1) ;
then A1: ((i - 2) / (2 |^ (n -' m))) + 1 < [\(((i - 2) / (2 |^ (n -' m))) + 2)/] by INT_1:def 6;
( (n -' m) + 1 >= 0 + 1 & (n -' m) + 1 <= 2 |^ (n -' m) ) by NEWTON:85, XREAL_1:6;
then 0 + 1 <= 2 |^ (n -' m) by XXREAL_0:2;
then A2: (- 1) / 1 <= (- 1) / (2 |^ (n -' m)) by XREAL_1:120;
assume 1 <= i ; :: thesis: [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT
then 1 - 2 <= i - 2 by XREAL_1:9;
then (- 1) / (2 |^ (n -' m)) <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:72;
then - 1 <= (i - 2) / (2 |^ (n -' m)) by A2, XXREAL_0:2;
then (- 1) + 1 <= ((i - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:6;
hence [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT by A1, INT_1:3; :: thesis: verum