let m, n be Nat; ( m < n implies (3 |^ m) - (3 to_power (1 - m)) < (3 |^ n) - (3 to_power (1 - n)) )
assume A1:
m < n
; (3 |^ m) - (3 to_power (1 - m)) < (3 |^ n) - (3 to_power (1 - n))
A2:
3 |^ m < 3 |^ n
by A1, Lm57, NAT_6:2;
1 - n < 1 - m
by A1, XREAL_1:15;
then
3 to_power (1 - n) < 3 to_power (1 - m)
by POWER:39;
hence
(3 |^ m) - (3 to_power (1 - m)) < (3 |^ n) - (3 to_power (1 - n))
by A2, XREAL_1:14; verum