let n be Nat; :: thesis: ( n > 1 implies ((3 |^ n) + (3 to_power (1 - n))) - 4 > 0 )
assume A1: n > 1 ; :: thesis: ((3 |^ n) + (3 to_power (1 - n))) - 4 > 0
set a = 3 to_power n;
A2: 3 to_power (1 - n) = (3 to_power 1) / (3 to_power n) by POWER:29
.= 3 / (3 to_power n) ;
A3: ((3 to_power n) * 3) / (3 to_power n) = 3 by XCMPLX_1:89;
A4: (3 to_power n) * (((3 to_power n) + (3 / (3 to_power n))) - 4) = (((3 to_power n) * (3 to_power n)) + (((3 to_power n) * 3) / (3 to_power n))) - (4 * (3 to_power n))
.= ((3 to_power n) - 1) * ((3 to_power n) - 3) by A3 ;
3 to_power n > 3 |^ 1 by A1, Lm57, NAT_6:2;
then A5: (3 to_power n) - 1 > 3 - 1 by XREAL_1:9;

now :: thesis: not ((3 to_power n) + (3 / (3 to_power n))) - 4 <= 0

assume ((3 to_power n) + (3 / (3 to_power n))) - 4 <= 0 ; :: thesis: contradiction
then (3 to_power n) - 3 <= 0 by A4, A5;
then ((3 to_power n) - 3) + 3 <= 0 + (3 |^ 1) by XREAL_1:6;
hence contradiction by A1, Lm57, NAT_6:2; :: thesis: verum

end;

hence ((3 |^ n) + (3 to_power (1 - n))) - 4 > 0 by A2; :: thesis: verum