<?xml version="1.0"?>
<div><span class="kw">theorem </span><a NAME="T312"><span class="comment"><font color="firebrick">:: XPRIMET1:312</font></span><br/></a><div class="add"> for <font color="Olive" title="b1">k</font> being   <a href="ordinal1.html#NM6" title="ORDINAL1:NM.6">Nat</a><br/>  for <font color="Olive" title="b2">p</font> being   <a href="int_2.html#NM1" title="INT_2:NM.1">Prime</a>  st <font color="Olive" title="b2">p</font> <a href="xcmplx_0.html#K3" title="XCMPLX_0:func.3">*</a> <font color="Olive" title="b2">p</font> <a href="xxreal_0.html#R1" title="XXREAL_0:pred.1">&lt;=</a> <font color="Olive" title="b1">k</font> &amp; <font color="Olive" title="b1">k</font> <a href="xxreal_0.html#NR3" title="XXREAL_0:NR.3">&lt;</a> 844561 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 2 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 3 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 5 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 7 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 11 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 13 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 17 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 19 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 23 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 29 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 31 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 37 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 41 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 43 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 47 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 53 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 59 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 61 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 67 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 71 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 73 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 79 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 83 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 89 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 97 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 101 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 103 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 107 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 109 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 113 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 127 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 131 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 137 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 139 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 149 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 151 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 157 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 163 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 167 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 173 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 179 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 181 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 191 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 193 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 197 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 199 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 211 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 223 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 227 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 229 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 233 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 239 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 241 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 251 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 257 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 263 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 269 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 271 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 277 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 281 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 283 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 293 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 307 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 311 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 313 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 317 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 331 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 337 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 347 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 349 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 353 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 359 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 367 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 373 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 379 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 383 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 389 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 397 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 401 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 409 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 419 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 421 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 431 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 433 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 439 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 443 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 449 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 457 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 461 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 463 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 467 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 479 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 487 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 491 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 499 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 503 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 509 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 521 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 523 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 541 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 547 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 557 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 563 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 569 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 571 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 577 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 587 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 593 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 599 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 601 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 607 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 613 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 617 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 619 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 631 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 641 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 643 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 647 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 653 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 659 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 661 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 673 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 677 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 683 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 691 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 701 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 709 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 719 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 727 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 733 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 739 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 743 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 751 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 757 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 761 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 769 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 773 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 787 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 797 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 809 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 811 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 821 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 823 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 827 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 829 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 839 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 853 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 857 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 859 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 863 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 877 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 881 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 883 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 887 &amp;  not <font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 907 holds <br/><font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 911</div></div>
