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

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

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:8; :: thesis: verum

end;

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

then A1: 1 + 1 <= m by NAT_1:13;
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:64;
then (2 * m) + (2 * 1) <= (2 * (2 |^ i)) + (2 * 3) ;
then (2 * m) + (2 * 1) <= (2 |^ (i + 1)) + 6 by NEWTON:6;
then ((2 * m) + 2) - 4 <= ((2 |^ (i + 1)) + 6) - 4 by XREAL_1:9;
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:6;
hence (2 * m) -' 2 < (2 |^ (i + 1)) + 3 by A2, XXREAL_0:2; :: thesis: verum

end;

end;