let n be Nat; :: thesis: ( n > 1 implies ((3 |^ n) - (3 to_power (1 - n))) - 2 > 0 )
assume A1: n > 1 ; :: thesis: ((3 |^ n) - (3 to_power (1 - n))) - 2 > 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))) - 2) = (((3 to_power n) * (3 to_power n)) - (((3 to_power n) * 3) / (3 to_power n))) - (2 * (3 to_power n))
.= ((3 to_power n) + 1) * ((3 to_power n) - 3) by A3 ;

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

assume ((3 to_power n) - (3 / (3 to_power n))) - 2 <= 0 ; :: thesis: contradiction
then (3 to_power n) - 3 <= 0 by A4;
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))) - 2 > 0 by A2; :: thesis: verum