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