theorem :: XPRIMET1:212

for k being Nat
for p being Prime st p * p <= k & k < 344569 & not p = 2 & not p = 3 & not p = 5 & not p = 7 & not p = 11 & not p = 13 & not p = 17 & not p = 19 & not p = 23 & not p = 29 & not p = 31 & not p = 37 & not p = 41 & not p = 43 & not p = 47 & not p = 53 & not p = 59 & not p = 61 & not p = 67 & not p = 71 & not p = 73 & not p = 79 & not p = 83 & not p = 89 & not p = 97 & not p = 101 & not p = 103 & not p = 107 & not p = 109 & not p = 113 & not p = 127 & not p = 131 & not p = 137 & not p = 139 & not p = 149 & not p = 151 & not p = 157 & not p = 163 & not p = 167 & not p = 173 & not p = 179 & not p = 181 & not p = 191 & not p = 193 & not p = 197 & not p = 199 & not p = 211 & not p = 223 & not p = 227 & not p = 229 & not p = 233 & not p = 239 & not p = 241 & not p = 251 & not p = 257 & not p = 263 & not p = 269 & not p = 271 & not p = 277 & not p = 281 & not p = 283 & not p = 293 & not p = 307 & not p = 311 & not p = 313 & not p = 317 & not p = 331 & not p = 337 & not p = 347 & not p = 349 & not p = 353 & not p = 359 & not p = 367 & not p = 373 & not p = 379 & not p = 383 & not p = 389 & not p = 397 & not p = 401 & not p = 409 & not p = 419 & not p = 421 & not p = 431 & not p = 433 & not p = 439 & not p = 443 & not p = 449 & not p = 457 & not p = 461 & not p = 463 & not p = 467 & not p = 479 & not p = 487 & not p = 491 & not p = 499 & not p = 503 & not p = 509 & not p = 521 & not p = 523 & not p = 541 & not p = 547 & not p = 557 & not p = 563 & not p = 569 & not p = 571 holds
p = 577