let m be Nat; (2 |^ (3 + m)) + (2 |^ (3 + m)) < 3 |^ (3 + m)
A4: (2 |^ (2 + 1)) + (2 |^ (2 + 1)) =
2 * (2 |^ (2 + 1))
.=
2 * (2 * (2 |^ 2))
by NEWTON:6
.=
2 * ((2 * 2) * 2)
by NEWTON:81
;
A5: 3 |^ (2 + 1) =
3 * (3 |^ 2)
by NEWTON:6
.=
(3 * 3) * 3
by NEWTON:81
;
A6:
( 2 |^ (3 + m) = (2 |^ 3) * (2 |^ m) & 3 |^ (3 + m) = (3 |^ 3) * (3 |^ m) )
by NEWTON:8;
2 |^ m <= 3 |^ m
by Lm3a;
then A7:
((2 |^ 3) + (2 |^ 3)) * (2 |^ m) <= ((2 |^ 3) + (2 |^ 3)) * (3 |^ m)
by XREAL_1:64;
3 |^ m > 0
by PREPOWER:6;
then
((2 |^ 3) + (2 |^ 3)) * (3 |^ m) < (3 |^ 3) * (3 |^ m)
by A4, A5, XREAL_1:68;
hence
(2 |^ (3 + m)) + (2 |^ (3 + m)) < 3 |^ (3 + m)
by XXREAL_0:2, A6, A7; verum