thus (5 * (2 |^ (2 |^ 1))) + 1 is composite by Lm2, XPRIMES0:21; :: according to NUMBER13:def 5 :: thesis: for m being positive Nat st m < 1 holds
not (5 * (2 |^ (2 |^ m))) + 1 is composite
thus for m being positive Nat st m < 1 holds
not (5 * (2 |^ (2 |^ m))) + 1 is composite by NAT_1:14; :: thesis: verum