let n be Nat; :: thesis: ( n > 1 implies ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 273 )
assume A1: n > 1 ; :: thesis: ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 273
then n + 1 > 1 + 1 by XREAL_1:6;
then n + 1 >= 2 + 1 by NAT_1:13;
then 2 |^ (n + 1) >= 2 |^ 3 by PREPOWER:93;
then A2: 2 |^ (2 |^ (n + 1)) >= 2 |^ 8 by Lm3, PREPOWER:93;
n >= 1 + 1 by A1, NAT_1:13;
then 2 |^ n >= 2 |^ 2 by PREPOWER:93;
then 2 |^ (2 |^ n) >= 2 |^ 4 by Lm2, PREPOWER:93;
then (2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n)) >= 256 + 16 by A2, Lm4, Lm6, XREAL_1:7;
then ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 272 + 1 by XREAL_1:6;
hence ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 273 ; :: thesis: verum