let n be Nat; :: thesis: ( n > 0 implies ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 21 )
assume n > 0 ; :: thesis: ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 21
then A1: n >= 0 + 1 by NAT_1:13;
then n + 1 >= 1 + 1 by XREAL_1:6;
then 2 |^ (n + 1) >= 2 |^ 2 by PREPOWER:93;
then A2: 2 |^ (2 |^ (n + 1)) >= 2 |^ 4 by Lm2, PREPOWER:93;
2 |^ n >= 2 |^ 1 by A1, PREPOWER:93;
then 2 |^ (2 |^ n) >= 2 |^ 2 by PREPOWER:93;
then (2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n)) >= 16 + 4 by A2, Lm2, Lm4, XREAL_1:7;
then ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 20 + 1 by XREAL_1:6;
hence ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 21 ; :: thesis: verum