let k be Nat; :: thesis: (10 |^ ((6 * k) + 4)) + 3 is composite
set z = (10 |^ ((6 * k) + 4)) + 3;
0 + 2 <= (10 |^ ((6 * k) + 4)) + 3 by XREAL_1:7;
hence 2 <= (10 |^ ((6 * k) + 4)) + 3 ; :: according to NUMBER02:def 1 :: thesis: not (10 |^ ((6 * k) + 4)) + 3 is prime
0 + 1 < (6 * k) + 4 by XREAL_1:8;
then 10 |^ 1 < 10 |^ ((6 * k) + 4) by PEPIN:66;
then 10 + 3 < (10 |^ ((6 * k) + 4)) + 3 by XREAL_1:8;
then 7 < (10 |^ ((6 * k) + 4)) + 3 by XXREAL_0:2;
hence not (10 |^ ((6 * k) + 4)) + 3 is prime by Th65; :: thesis: verum