:: deftheorem defines satisfies_Sierpinski_problem_121_for NUMBER13:def 5 :
for k, n being Nat holds
( n satisfies_Sierpinski_problem_121_for k iff ( (k * (2 |^ (2 |^ n))) + 1 is composite & ( for m being positive Nat st m < n holds
not (k * (2 |^ (2 |^ m))) + 1 is composite ) ) );