let a, n be Nat; :: thesis: ( a > 4 & n > 0 implies (a |^ (2 |^ n)) + 1 > 25 )
A1: 5 |^ 2 = 5 * 5 by WSIERP_1:1;
assume A2: a > 4 ; :: thesis: ( not n > 0 or (a |^ (2 |^ n)) + 1 > 25 )
then a >= 4 + 1 by NAT_1:13;
then A3: a |^ 2 >= 5 |^ 2 by NEWTON02:41;
A4: a >= 1 by A2, XXREAL_0:2;
assume n > 0 ; :: thesis: (a |^ (2 |^ n)) + 1 > 25
then 2 |^ n >= 1 + 1 by Lm1, NAT_1:13, PEPIN:66;
then a |^ (2 |^ n) >= a |^ 2 by A4, PREPOWER:93;
then a |^ (2 |^ n) >= 25 by A1, A3, XXREAL_0:2;
hence (a |^ (2 |^ n)) + 1 > 25 by NAT_1:13; :: thesis: verum