given n being Nat such that A1: n satisfies_Sierpinski_problem_89 and
n + 1 satisfies_Sierpinski_problem_89 and
n + 2 satisfies_Sierpinski_problem_89 and
A2: n + 3 satisfies_Sierpinski_problem_89 ; :: thesis: contradiction
A3: n is_a_product_of_two_different_primes by A1;
A4: n + 1 is_a_product_of_two_different_primes by A1;
A5: n + 2 is_a_product_of_two_different_primes by A1;
A6: n + 3 is_a_product_of_two_different_primes by A2;
per cases ( 4 divides n or 4 divides n + 1 or 4 divides n + 2 or 4 divides n + 3 ) by NUMBER06:19;
suppose A7: 4 divides n ; :: thesis: contradiction
consider p, q being Prime such that
A8: p <> q and
A9: n = p * q by A3;
A10: ( p divides p * q & q divides p * q ) ;
4 divides p * q by A9, A7;
then p * q = 4 by GR_CY_3:1, XPRIMES0:4;
then ( ( p = 1 or p = 2 ) & ( q = 1 or q = 2 ) ) by A10, NUMBER05:21;
hence contradiction by A8, INT_2:def 4; :: thesis: verum
end;
suppose A11: 4 divides n + 1 ; :: thesis: contradiction
consider p, q being Prime such that
A12: p <> q and
A13: n + 1 = p * q by A4;
A14: ( p divides p * q & q divides p * q ) ;
4 divides p * q by A13, A11;
then p * q = 4 by GR_CY_3:1, XPRIMES0:4;
then ( ( p = 1 or p = 2 ) & ( q = 1 or q = 2 ) ) by A14, NUMBER05:21;
hence contradiction by A12, INT_2:def 4; :: thesis: verum
end;
suppose A15: 4 divides n + 2 ; :: thesis: contradiction
consider p, q being Prime such that
A16: p <> q and
A17: n + 2 = p * q by A5;
A18: ( p divides p * q & q divides p * q ) ;
4 divides p * q by A17, A15;
then p * q = 4 by GR_CY_3:1, XPRIMES0:4;
then ( ( p = 1 or p = 2 ) & ( q = 1 or q = 2 ) ) by A18, NUMBER05:21;
hence contradiction by A16, INT_2:def 4; :: thesis: verum
end;
suppose A19: 4 divides n + 3 ; :: thesis: contradiction
consider p, q being Prime such that
A20: p <> q and
A21: n + 3 = p * q by A6;
A22: ( p divides p * q & q divides p * q ) ;
4 divides p * q by A21, A19;
then p * q = 4 by GR_CY_3:1, XPRIMES0:4;
then ( ( p = 1 or p = 2 ) & ( q = 1 or q = 2 ) ) by A22, NUMBER05:21;
hence contradiction by A20, INT_2:def 4; :: thesis: verum
end;
end;