let n be Nat; :: thesis: ( n satisfies_Sierpinski_problem_89 & n <= 201 implies n in {33,85,93,141,201} )
assume that
A1: n satisfies_Sierpinski_problem_89 and
A2: n <= 201 and
A3: not n in {33,85,93,141,201} ; :: thesis: contradiction
( 4 < 6 & 6 <= n ) by A1, Th65;
then A4: 4 < n by XXREAL_0:2;
set a = n div 4;
set b = n mod 4;
A5: n = ((n div 4) * 4) + (n mod 4) by INT_1:59;
A6: n mod 4 = 1
proof
n mod 4 < 3 + 1 by NAT_D:1;
then n mod 4 <= 3 by NAT_1:13;
then not not n mod 4 = 0 & ... & not n mod 4 = 3 ;
per cases then ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) ;
suppose n mod 4 = 0 ; :: thesis: n mod 4 = 1
then n = 4 * (n div 4) by A5;
then ( 4 <> n & 4 divides n ) by A4;
hence n mod 4 = 1 by A1, Th63, XPRIMES0:4; :: thesis: verum
end;
suppose n mod 4 = 1 ; :: thesis: n mod 4 = 1
hence n mod 4 = 1 ; :: thesis: verum
end;
suppose n mod 4 = 2 ; :: thesis: n mod 4 = 1
then n + 2 = 4 * ((n div 4) + 1) by A5;
then ( 4 <> n + 2 & 4 divides n + 2 ) by A4;
hence n mod 4 = 1 by A1, Th63, XPRIMES0:4; :: thesis: verum
end;
suppose n mod 4 = 3 ; :: thesis: n mod 4 = 1
then n + 1 = 4 * ((n div 4) + 1) by A5;
then ( 4 <> n + 1 & 4 divides n + 1 ) by A4, NAT_1:11;
hence n mod 4 = 1 by A1, Th63, XPRIMES0:4; :: thesis: verum
end;
end;
end;
A7: n div 4 <> 0 by A4, A5, A6;
((n div 4) * 4) + 1 <= (50 * 4) + 1 by A2, A5, A6;
then (n div 4) * 4 <= 50 * 4 by XREAL_1:6;
then ( 1 <= n div 4 & n div 4 <= 50 ) by XREAL_1:68, A7, NAT_1:14;
then not not n = (1 * 4) + 1 & ... & not n = (50 * 4) + 1 by A5, A6;
per cases then ( n = 5 or n = 9 or n = 13 or n = 17 or n = 21 or n = 25 or n = 29 or n = 37 or n = 41 or n = 45 or n = 49 or n = 53 or n = 57 or n = 61 or n = 65 or n = 69 or n = 73 or n = 77 or n = 81 or n = 89 or n = 97 or n = 101 or n = 105 or n = 109 or n = 113 or n = 117 or n = 121 or n = 125 or n = 129 or n = 133 or n = 137 or n = 145 or n = 149 or n = 153 or n = 157 or n = 161 or n = 165 or n = 169 or n = 173 or n = 177 or n = 181 or n = 185 or n = 189 or n = 193 or n = 197 ) by A3, ENUMSET1:def 3;
suppose n = 5 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:5; :: thesis: verum
end;
suppose n = 9 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:11; :: thesis: verum
end;
suppose n = 13 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:13; :: thesis: verum
end;
suppose n = 17 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:17; :: thesis: verum
end;
suppose n = 21 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:23; :: thesis: verum
end;
suppose A: n = 25 ; :: thesis: contradiction
25 = 5 * 5 ;
hence contradiction by A1, A, Th64, XPRIMES1:5; :: thesis: verum
end;
suppose n = 29 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:29; :: thesis: verum
end;
suppose n = 37 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:37; :: thesis: verum
end;
suppose n = 41 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:41; :: thesis: verum
end;
suppose n = 45 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:47; :: thesis: verum
end;
suppose A: n = 49 ; :: thesis: contradiction
49 = 7 * 7 ;
hence contradiction by A1, A, Th64, XPRIMES1:7; :: thesis: verum
end;
suppose n = 53 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:53; :: thesis: verum
end;
suppose n = 57 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:59; :: thesis: verum
end;
suppose n = 61 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:61; :: thesis: verum
end;
suppose n = 65 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:67; :: thesis: verum
end;
suppose n = 69 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:71; :: thesis: verum
end;
suppose n = 73 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:73; :: thesis: verum
end;
suppose n = 77 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:79; :: thesis: verum
end;
suppose n = 81 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:83; :: thesis: verum
end;
suppose n = 89 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:89; :: thesis: verum
end;
suppose n = 97 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:97; :: thesis: verum
end;
suppose n = 101 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:101; :: thesis: verum
end;
suppose n = 105 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:107; :: thesis: verum
end;
suppose n = 109 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:109; :: thesis: verum
end;
suppose n = 113 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:113; :: thesis: verum
end;
suppose A: n = 117 ; :: thesis: contradiction
9 divides 9 * 13 ;
hence contradiction by A1, A, Th63, XPRIMES0:9; :: thesis: verum
end;
suppose A: n = 121 ; :: thesis: contradiction
121 = 11 * 11 ;
hence contradiction by A1, A, Th64, XPRIMES1:11; :: thesis: verum
end;
suppose n = 125 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:127; :: thesis: verum
end;
suppose n = 129 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:131; :: thesis: verum
end;
suppose A: n = 133 ; :: thesis: contradiction
9 divides 9 * 15 ;
hence contradiction by A1, A, Th63, XPRIMES0:9; :: thesis: verum
end;
suppose n = 137 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:137; :: thesis: verum
end;
suppose A: n = 145 ; :: thesis: contradiction
21 divides 21 * 7 ;
hence contradiction by A1, A, Th63, XPRIMES0:21; :: thesis: verum
end;
suppose n = 149 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:149; :: thesis: verum
end;
suppose A: n = 153 ; :: thesis: contradiction
14 divides 14 * 11 ;
hence contradiction by A1, A, Th63, XPRIMES0:14; :: thesis: verum
end;
suppose n = 157 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:157; :: thesis: verum
end;
suppose n = 161 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:163; :: thesis: verum
end;
suppose n = 165 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:167; :: thesis: verum
end;
suppose A: n = 169 ; :: thesis: contradiction
169 = 13 * 13 ;
hence contradiction by A1, A, Th64, XPRIMES1:13; :: thesis: verum
end;
suppose n = 173 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:173; :: thesis: verum
end;
suppose n = 177 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:179; :: thesis: verum
end;
suppose n = 181 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:181; :: thesis: verum
end;
suppose A: n = 185 ; :: thesis: contradiction
6 divides 6 * 31 ;
hence contradiction by A1, A, Th63, XPRIMES0:6; :: thesis: verum
end;
suppose n = 189 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:191; :: thesis: verum
end;
suppose n = 193 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:193; :: thesis: verum
end;
suppose n = 197 ; :: thesis: contradiction
hence contradiction by A1, Th61, XPRIMES1:197; :: thesis: verum
end;
end;