set n = 3;
thus (7 * (2 |^ (2 |^ 3))) + 1 is composite by Lm3, Lm6, XPRIMES0:1793; :: according to NUMBER13:def 5 :: thesis: for m being positive Nat st m < 3 holds
not (7 * (2 |^ (2 |^ m))) + 1 is composite
let m be positive Nat; :: thesis: ( m < 3 implies not (7 * (2 |^ (2 |^ m))) + 1 is composite )
assume m < 3 ; :: thesis: not (7 * (2 |^ (2 |^ m))) + 1 is composite
per cases then ( m = 0 or m = 1 or m = 2 ) by Th1;
suppose m = 0 ; :: thesis: not (7 * (2 |^ (2 |^ m))) + 1 is composite
hence not (7 * (2 |^ (2 |^ m))) + 1 is composite ; :: thesis: verum
end;
suppose m = 1 ; :: thesis: not (7 * (2 |^ (2 |^ m))) + 1 is composite
hence not (7 * (2 |^ (2 |^ m))) + 1 is composite by Lm2, XPRIMES1:29; :: thesis: verum
end;
suppose m = 2 ; :: thesis: not (7 * (2 |^ (2 |^ m))) + 1 is composite
hence not (7 * (2 |^ (2 |^ m))) + 1 is composite by Lm2, Lm4, XPRIMES1:113; :: thesis: verum
end;
end;