let n be Nat; :: thesis: (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0
A1: ( (- 1) |^ (n + 3) = |.((- 1) |^ (n + 3)).| or - ((- 1) |^ (n + 3)) = |.((- 1) |^ (n + 3)).| ) by ABSVALUE:1;
A2: |.((- 1) |^ (n + 3)).| = 1 by Th1;
n + 3 >= 3 by NAT_1:11;
then n + 3 > 0 by XXREAL_0:2;
then 2 |^ (n + 3) > 1 by PEPIN:25;
then A3: (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 1 + ((- 1) |^ (n + 3)) by XREAL_1:8;

per cases ( (- 1) |^ (n + 3) = - 1 or (- 1) |^ (n + 3) = 1 ) by A2, A1;

suppose (- 1) |^ (n + 3) = - 1 ; :: thesis: (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0

hence (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0 by A3; :: thesis: verum

end;

suppose (- 1) |^ (n + 3) = 1 ; :: thesis: (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0

hence (2 |^ (n + 3)) + ((- 1) |^ (n + 3)) > 0 by A3, XXREAL_0:2; :: thesis: verum

end;

end;