let k, n be Nat; :: thesis: ( k > 0 & n = (28 * k) + 1 implies (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite )
assume that
A1: k > 0 and
A2: n = (28 * k) + 1 ; :: thesis: (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite
set x = (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2);
A3: ((2 |^ (2 * n)) + 1) |^ 2 = ((2 |^ (2 * n)) + 1) ^2 by WSIERP_1:1;
A4: 2 |^ (2 * n) = 4 |^ n by Lm1, NEWTON:9;
k >= 0 + 1 by A1, NAT_1:13;
then 28 * k >= 28 * 1 by XREAL_1:64;
then (28 * k) + 1 >= 28 + 1 by XREAL_1:6;
then (28 * k) + 1 > 1 by XXREAL_0:2;
then 4 |^ n > 4 |^ 1 by A2, PEPIN:66;
then (2 |^ (2 * n)) + 1 > 4 + 1 by A4, XREAL_1:8;
then ((2 |^ (2 * n)) + 1) ^2 > 5 * 5 by XREAL_1:96;
then A5: (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) > 25 + 4 by A3, Lm1, XREAL_1:8;
assume not (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is composite ; :: thesis: contradiction
then (((2 |^ (2 * n)) + 1) |^ 2) + (2 |^ 2) is prime by A5, XXREAL_0:2, NUMBER02:def 1;
hence contradiction by A2, A5, Th77; :: thesis: verum