333331 = (2 * 166665) + 1 ;
hence not 2 divides 333331 ; :: thesis:
333331 = (3 * 111110) + 1 ;
hence not 3 divides 333331 by NAT_4:9; :: thesis:
333331 = (5 * 66666) + 1 ;
hence not 5 divides 333331 by NAT_4:9; :: thesis:
333331 = (7 * 47618) + 5 ;
hence not 7 divides 333331 by NAT_4:9; :: thesis:
333331 = (11 * 30302) + 9 ;
hence not 11 divides 333331 by NAT_4:9; :: thesis:
333331 = (13 * 25640) + 11 ;
hence not 13 divides 333331 by NAT_4:9; :: thesis:
333331 = (17 * 19607) + 12 ;
hence not 17 divides 333331 by NAT_4:9; :: thesis:
333331 = (19 * 17543) + 14 ;
hence not 19 divides 333331 by NAT_4:9; :: thesis:
333331 = (23 * 14492) + 15 ;
hence not 23 divides 333331 by NAT_4:9; :: thesis:
333331 = (29 * 11494) + 5 ;
hence not 29 divides 333331 by NAT_4:9; :: thesis:
333331 = (31 * 10752) + 19 ;
hence not 31 divides 333331 by NAT_4:9; :: thesis:
333331 = (37 * 9008) + 35 ;
hence not 37 divides 333331 by NAT_4:9; :: thesis:
333331 = (41 * 8130) + 1 ;
hence not 41 divides 333331 by NAT_4:9; :: thesis:
333331 = (43 * 7751) + 38 ;
hence not 43 divides 333331 by NAT_4:9; :: thesis:
333331 = (47 * 7092) + 7 ;
hence not 47 divides 333331 by NAT_4:9; :: thesis:
333331 = (53 * 6289) + 14 ;
hence not 53 divides 333331 by NAT_4:9; :: thesis:
333331 = (59 * 5649) + 40 ;
hence not 59 divides 333331 by NAT_4:9; :: thesis:
333331 = (61 * 5464) + 27 ;
hence not 61 divides 333331 by NAT_4:9; :: thesis:
333331 = (67 * 4975) + 6 ;
hence not 67 divides 333331 by NAT_4:9; :: thesis:
333331 = (71 * 4694) + 57 ;
hence not 71 divides 333331 by NAT_4:9; :: thesis:
333331 = (73 * 4566) + 13 ;
hence not 73 divides 333331 by NAT_4:9; :: thesis:
333331 = (79 * 4219) + 30 ;
hence not 79 divides 333331 by NAT_4:9; :: thesis:
333331 = (83 * 4016) + 3 ;
hence not 83 divides 333331 by NAT_4:9; :: thesis:
333331 = (89 * 3745) + 26 ;
hence not 89 divides 333331 by NAT_4:9; :: thesis:
333331 = (97 * 3436) + 39 ;
hence not 97 divides 333331 by NAT_4:9; :: thesis:
333331 = (101 * 3300) + 31 ;
hence not 101 divides 333331 by NAT_4:9; :: thesis:
333331 = (103 * 3236) + 23 ;
hence not 103 divides 333331 by NAT_4:9; :: thesis:
333331 = (107 * 3115) + 26 ;
hence not 107 divides 333331 by NAT_4:9; :: thesis:
333331 = (109 * 3058) + 9 ;
hence not 109 divides 333331 by NAT_4:9; :: thesis:
333331 = (113 * 2949) + 94 ;
hence not 113 divides 333331 by NAT_4:9; :: thesis:
333331 = (127 * 2624) + 83 ;
hence not 127 divides 333331 by NAT_4:9; :: thesis:
333331 = (131 * 2544) + 67 ;
hence not 131 divides 333331 by NAT_4:9; :: thesis:
333331 = (137 * 2433) + 10 ;
hence not 137 divides 333331 by NAT_4:9; :: thesis:
333331 = (139 * 2398) + 9 ;
hence not 139 divides 333331 by NAT_4:9; :: thesis:
333331 = (149 * 2237) + 18 ;
hence not 149 divides 333331 by NAT_4:9; :: thesis:
333331 = (151 * 2207) + 74 ;
hence not 151 divides 333331 by NAT_4:9; :: thesis:
333331 = (157 * 2123) + 20 ;
hence not 157 divides 333331 by NAT_4:9; :: thesis:
333331 = (163 * 2044) + 159 ;
hence not 163 divides 333331 by NAT_4:9; :: thesis:
333331 = (167 * 1995) + 166 ;
hence not 167 divides 333331 by NAT_4:9; :: thesis:
333331 = (173 * 1926) + 133 ;
hence not 173 divides 333331 by NAT_4:9; :: thesis:
333331 = (179 * 1862) + 33 ;
hence not 179 divides 333331 by NAT_4:9; :: thesis:
333331 = (181 * 1841) + 110 ;
hence not 181 divides 333331 by NAT_4:9; :: thesis:
333331 = (191 * 1745) + 36 ;
hence not 191 divides 333331 by NAT_4:9; :: thesis:
333331 = (193 * 1727) + 20 ;
hence not 193 divides 333331 by NAT_4:9; :: thesis:
333331 = (197 * 1692) + 7 ;
hence not 197 divides 333331 by NAT_4:9; :: thesis:
333331 = (199 * 1675) + 6 ;
hence not 199 divides 333331 by NAT_4:9; :: thesis:
333331 = (211 * 1579) + 162 ;
hence not 211 divides 333331 by NAT_4:9; :: thesis:
333331 = (223 * 1494) + 169 ;
hence not 223 divides 333331 by NAT_4:9; :: thesis:
333331 = (227 * 1468) + 95 ;
hence not 227 divides 333331 by NAT_4:9; :: thesis:
333331 = (229 * 1455) + 136 ;
hence not 229 divides 333331 by NAT_4:9; :: thesis:
333331 = (233 * 1430) + 141 ;
hence not 233 divides 333331 by NAT_4:9; :: thesis:
333331 = (239 * 1394) + 165 ;
hence not 239 divides 333331 by NAT_4:9; :: thesis:
333331 = (241 * 1383) + 28 ;
hence not 241 divides 333331 by NAT_4:9; :: thesis:
333331 = (251 * 1328) + 3 ;
hence not 251 divides 333331 by NAT_4:9; :: thesis:
333331 = (257 * 1297) + 2 ;
hence not 257 divides 333331 by NAT_4:9; :: thesis:
333331 = (263 * 1267) + 110 ;
hence not 263 divides 333331 by NAT_4:9; :: thesis:
333331 = (269 * 1239) + 40 ;
hence not 269 divides 333331 by NAT_4:9; :: thesis:
333331 = (271 * 1230) + 1 ;
hence not 271 divides 333331 by NAT_4:9; :: thesis:
333331 = (277 * 1203) + 100 ;
hence not 277 divides 333331 by NAT_4:9; :: thesis:
333331 = (281 * 1186) + 65 ;
hence not 281 divides 333331 by NAT_4:9; :: thesis:
333331 = (283 * 1177) + 240 ;
hence not 283 divides 333331 by NAT_4:9; :: thesis:
333331 = (293 * 1137) + 190 ;
hence not 293 divides 333331 by NAT_4:9; :: thesis:
333331 = (307 * 1085) + 236 ;
hence not 307 divides 333331 by NAT_4:9; :: thesis:
333331 = (311 * 1071) + 250 ;
hence not 311 divides 333331 by NAT_4:9; :: thesis:
333331 = (313 * 1064) + 299 ;
hence not 313 divides 333331 by NAT_4:9; :: thesis:
333331 = (317 * 1051) + 164 ;
hence not 317 divides 333331 by NAT_4:9; :: thesis:
333331 = (331 * 1007) + 14 ;
hence not 331 divides 333331 by NAT_4:9; :: thesis:
333331 = (337 * 989) + 38 ;
hence not 337 divides 333331 by NAT_4:9; :: thesis:
333331 = (347 * 960) + 211 ;
hence not 347 divides 333331 by NAT_4:9; :: thesis:
333331 = (349 * 955) + 36 ;
hence not 349 divides 333331 by NAT_4:9; :: thesis:
333331 = (353 * 944) + 99 ;
hence not 353 divides 333331 by NAT_4:9; :: thesis:
333331 = (359 * 928) + 179 ;
hence not 359 divides 333331 by NAT_4:9; :: thesis:
333331 = (367 * 908) + 95 ;
hence not 367 divides 333331 by NAT_4:9; :: thesis:
333331 = (373 * 893) + 242 ;
hence not 373 divides 333331 by NAT_4:9; :: thesis:
333331 = (379 * 879) + 190 ;
hence not 379 divides 333331 by NAT_4:9; :: thesis:
333331 = (383 * 870) + 121 ;
hence not 383 divides 333331 by NAT_4:9; :: thesis:
333331 = (389 * 856) + 347 ;
hence not 389 divides 333331 by NAT_4:9; :: thesis:
333331 = (397 * 839) + 248 ;
hence not 397 divides 333331 by NAT_4:9; :: thesis:
333331 = (401 * 831) + 100 ;
hence not 401 divides 333331 by NAT_4:9; :: thesis:
333331 = (409 * 814) + 405 ;
hence not 409 divides 333331 by NAT_4:9; :: thesis:
333331 = (419 * 795) + 226 ;
hence not 419 divides 333331 by NAT_4:9; :: thesis:
333331 = (421 * 791) + 320 ;
hence not 421 divides 333331 by NAT_4:9; :: thesis:
333331 = (431 * 773) + 168 ;
hence not 431 divides 333331 by NAT_4:9; :: thesis:
333331 = (433 * 769) + 354 ;
hence not 433 divides 333331 by NAT_4:9; :: thesis:
333331 = (439 * 759) + 130 ;
hence not 439 divides 333331 by NAT_4:9; :: thesis:
333331 = (443 * 752) + 195 ;
hence not 443 divides 333331 by NAT_4:9; :: thesis:
333331 = (449 * 742) + 173 ;
hence not 449 divides 333331 by NAT_4:9; :: thesis:
333331 = (457 * 729) + 178 ;
hence not 457 divides 333331 by NAT_4:9; :: thesis:
333331 = (461 * 723) + 28 ;
hence not 461 divides 333331 by NAT_4:9; :: thesis:
333331 = (463 * 719) + 434 ;
hence not 463 divides 333331 by NAT_4:9; :: thesis:
333331 = (467 * 713) + 360 ;
hence not 467 divides 333331 by NAT_4:9; :: thesis:
333331 = (479 * 695) + 426 ;
hence not 479 divides 333331 by NAT_4:9; :: thesis:
333331 = (487 * 684) + 223 ;
hence not 487 divides 333331 by NAT_4:9; :: thesis:
333331 = (491 * 678) + 433 ;
hence not 491 divides 333331 by NAT_4:9; :: thesis:
333331 = (499 * 667) + 498 ;
hence not 499 divides 333331 by NAT_4:9; :: thesis:
333331 = (503 * 662) + 345 ;
hence not 503 divides 333331 by NAT_4:9; :: thesis:
333331 = (509 * 654) + 445 ;
hence not 509 divides 333331 by NAT_4:9; :: thesis:
333331 = (521 * 639) + 412 ;
hence not 521 divides 333331 by NAT_4:9; :: thesis:
333331 = (523 * 637) + 180 ;
hence not 523 divides 333331 by NAT_4:9; :: thesis:
333331 = (541 * 616) + 75 ;
hence not 541 divides 333331 by NAT_4:9; :: thesis:
333331 = (547 * 609) + 208 ;
hence not 547 divides 333331 by NAT_4:9; :: thesis:
333331 = (557 * 598) + 245 ;
hence not 557 divides 333331 by NAT_4:9; :: thesis:
333331 = (563 * 592) + 35 ;
hence not 563 divides 333331 by NAT_4:9; :: thesis:
333331 = (569 * 585) + 466 ;
hence not 569 divides 333331 by NAT_4:9; :: thesis:
333331 = (571 * 583) + 438 ;
hence not 571 divides 333331 by NAT_4:9; :: thesis:
333331 = (577 * 577) + 402 ;
hence not 577 divides 333331 by NAT_4:9; :: thesis:

end;

then for n being Element of NAT st 1 < n & n * n <= 333331 & n is prime holds
not n divides 333331 by XPRIMET1:212;
hence 333331 is prime by NAT_4:14; :: thesis: