let s be positive Nat; :: thesis: (2 |^ (2 |^ ((10 * s) + 1))) + 19 is composite
set m = (2 |^ (2 |^ ((10 * s) + 1))) + 19;
A1: (2 |^ (2 |^ ((10 * s) + 1))) + 19 >= (2 |^ 2048) + 19 by Lm17, XREAL_1:6;
2 <= ((2 |^ 2048) + 17) + 2 by NAT_1:11;
hence (2 |^ (2 |^ ((10 * s) + 1))) + 19 >= 2 by A1, XXREAL_0:2; :: according to NUMBER02:def 1 :: thesis: not (2 |^ (2 |^ ((10 * s) + 1))) + 19 is prime
(2 |^ (2 |^ ((10 * s) + 1))) + 19 <> 23 by Lm17, Lm1, PEPIN:66;
hence not (2 |^ (2 |^ ((10 * s) + 1))) + 19 is prime by Th80; :: thesis: verum