set n = 5;
(2 |^ 32) + 1 >= 1 + 1 by XREAL_1:6, NAT_1:14;
hence (1 * (2 |^ (2 |^ 5))) + 1 is composite by Lm5, NAT_6:44; :: according to NUMBER13:def 5 :: thesis: for m being positive Nat st m < 5 holds
not (1 * (2 |^ (2 |^ m))) + 1 is composite
let m be positive Nat; :: thesis: ( m < 5 implies not (1 * (2 |^ (2 |^ m))) + 1 is composite )
assume m < 5 ; :: thesis: not (1 * (2 |^ (2 |^ m))) + 1 is composite

per cases then ( m = 0 or m = 1 or m = 2 or m = 3 or m = 4 ) by Th3;

suppose m = 0 ; :: thesis: not (1 * (2 |^ (2 |^ m))) + 1 is composite

hence not (1 * (2 |^ (2 |^ m))) + 1 is composite ; :: thesis: verum

end;

suppose m = 1 ; :: thesis: not (1 * (2 |^ (2 |^ m))) + 1 is composite

hence not (1 * (2 |^ (2 |^ m))) + 1 is composite by Lm2, XPRIMES1:5; :: thesis: verum

end;

suppose m = 2 ; :: thesis: not (1 * (2 |^ (2 |^ m))) + 1 is composite

hence not (1 * (2 |^ (2 |^ m))) + 1 is composite by Lm2, Lm4, XPRIMES1:17; :: thesis: verum

end;

suppose m = 3 ; :: thesis: not (1 * (2 |^ (2 |^ m))) + 1 is composite

hence not (1 * (2 |^ (2 |^ m))) + 1 is composite by Lm3, Lm6, XPRIMES1:257; :: thesis: verum

end;

suppose m = 4 ; :: thesis: not (1 * (2 |^ (2 |^ m))) + 1 is composite

hence not (1 * (2 |^ (2 |^ m))) + 1 is composite by Lm4, Lm7, PEPIN:62; :: thesis: verum

end;

end;