given p being Prime such that A1: p <= 130 and
A2: p satisfies_Sierpinski_problem_105 ; :: thesis: contradiction
p < 130 + 1 by A1, NAT_1:13;
per cases then ( p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53 or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 or p = 79 or p = 83 or p = 89 or p = 97 or p = 101 or p = 103 or p = 107 or p = 109 or p = 113 or p = 127 ) by XPRIMET1:61;
suppose p = 2 ; :: thesis: contradiction
hence contradiction by A2, Th81; :: thesis: verum
end;
suppose p = 3 ; :: thesis: contradiction
hence contradiction by A2, Th81; :: thesis: verum
end;
suppose p = 5 ; :: thesis: contradiction
hence contradiction by A2, Th81; :: thesis: verum
end;
suppose p = 7 ; :: thesis: contradiction
hence contradiction by A2, Th81; :: thesis: verum
end;
suppose p = 11 ; :: thesis: contradiction
hence contradiction by A2, Th81; :: thesis: verum
end;
suppose p = 13 ; :: thesis: contradiction
hence contradiction by A2, Th81; :: thesis: verum
end;
suppose p = 17 ; :: thesis: contradiction
hence contradiction by A2, Th81; :: thesis: verum
end;
suppose p = 19 ; :: thesis: contradiction
hence contradiction by A2, Th81; :: thesis: verum
end;
suppose p = 23 ; :: thesis: contradiction
hence contradiction by A2, Th81; :: thesis: verum
end;
suppose p = 29 ; :: thesis: contradiction
hence contradiction by A2, Th81; :: thesis: verum
end;
suppose p = 31 ; :: thesis: contradiction
hence contradiction by A2, Lm6, XPRIMES1:2; :: thesis: verum
end;
suppose p = 37 ; :: thesis: contradiction
hence contradiction by A2, Lm38; :: thesis: verum
end;
suppose p = 41 ; :: thesis: contradiction
hence contradiction by A2, Lm39; :: thesis: verum
end;
suppose p = 43 ; :: thesis: contradiction
hence contradiction by A2, Lm40; :: thesis: verum
end;
suppose p = 47 ; :: thesis: contradiction
hence contradiction by A2, Lm41; :: thesis: verum
end;
suppose p = 53 ; :: thesis: contradiction
hence contradiction by A2, Lm42; :: thesis: verum
end;
suppose p = 59 ; :: thesis: contradiction
hence contradiction by A2, Lm43; :: thesis: verum
end;
suppose p = 61 ; :: thesis: contradiction
hence contradiction by A2, Lm44; :: thesis: verum
end;
suppose p = 67 ; :: thesis: contradiction
hence contradiction by A2, Lm45; :: thesis: verum
end;
suppose p = 71 ; :: thesis: contradiction
hence contradiction by A2, Lm46; :: thesis: verum
end;
suppose p = 73 ; :: thesis: contradiction
hence contradiction by A2, Lm47; :: thesis: verum
end;
suppose p = 79 ; :: thesis: contradiction
hence contradiction by A2, Lm48; :: thesis: verum
end;
suppose p = 83 ; :: thesis: contradiction
hence contradiction by A2, Lm49; :: thesis: verum
end;
suppose p = 89 ; :: thesis: contradiction
hence contradiction by A2, Lm50; :: thesis: verum
end;
suppose p = 97 ; :: thesis: contradiction
hence contradiction by A2, Lm51; :: thesis: verum
end;
suppose p = 101 ; :: thesis: contradiction
hence contradiction by A2, Lm52; :: thesis: verum
end;
suppose p = 103 ; :: thesis: contradiction
hence contradiction by A2, Lm53; :: thesis: verum
end;
suppose p = 107 ; :: thesis: contradiction
hence contradiction by A2, Lm54; :: thesis: verum
end;
suppose p = 109 ; :: thesis: contradiction
hence contradiction by A2, Lm55; :: thesis: verum
end;
suppose p = 113 ; :: thesis: contradiction
hence contradiction by A2, Lm56; :: thesis: verum
end;
suppose p = 127 ; :: thesis: contradiction
hence contradiction by A2, Lm7, XPRIMES1:2; :: thesis: verum
end;
end;