let n be positive Nat; :: thesis: (5 * (2 |^ (2 |^ n))) + 1 is composite
H₁(5,n) >= (5 * 2) + 1 by Lm16;
hence H₁(5,n) >= 2 by XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (5 * (2 |^ (2 |^ n))) + 1 is prime
A1: (5 * (2 |^ (2 |^ n))) + 1 <> 3 by Lm16;
5 = (3 * 1) + 2 ;
hence not (5 * (2 |^ (2 |^ n))) + 1 is prime by A1, Th34; :: thesis: verum