let m, i be Element of NAT ; :: thesis: ( m < (2 |^ i) + 3 implies (2 * m) -' 2 < (2 |^ (i + 1)) + 3 )

per cases ( m = 0 or m = 1 or 2 <= m ) by NAT_1:27;

suppose ( m = 0 or m = 1 ) ; :: thesis: ( m < (2 |^ i) + 3 implies (2 * m) -' 2 < (2 |^ (i + 1)) + 3 )

hence ( m < (2 |^ i) + 3 implies (2 * m) -' 2 < (2 |^ (i + 1)) + 3 ) by NAT_2:10; :: thesis: verum

end;

suppose A1: 2 <= m ; :: thesis: ( m < (2 |^ i) + 3 implies (2 * m) -' 2 < (2 |^ (i + 1)) + 3 )

assume m < (2 |^ i) + 3 ; :: thesis: (2 * m) -' 2 < (2 |^ (i + 1)) + 3
then m + 1 <= (2 |^ i) + 3 by NAT_1:13;
then 2 * (m + 1) <= 2 * ((2 |^ i) + 3) by XREAL_1:66;
then (2 * m) + (2 * 1) <= (2 * (2 |^ i)) + (2 * 3) ;
then (2 * m) + (2 * 1) <= (2 |^ (i + 1)) + 6 by NEWTON:11;
then ((2 * m) + 2) - 4 <= ((2 |^ (i + 1)) + 6) - 4 by XREAL_1:11;
then (2 * m) - 2 <= (2 |^ (i + 1)) + 2 ;
then A2: (2 * m) -' 2 <= (2 |^ (i + 1)) + 2 by A1, Lm7;
(2 |^ (i + 1)) + 2 < (2 |^ (i + 1)) + 3 by XREAL_1:8;
hence (2 * m) -' 2 < (2 |^ (i + 1)) + 3 by A2, XXREAL_0:2; :: thesis: verum

end;

end;