<?xml version="1.0"?>
<div><span class="kw">theorem </span><a NAME="T114"><span class="comment"><font color="firebrick">:: XPRIMET1:114</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> 73441 &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 holds <br/><font color="Olive" title="b2">p</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> 269</div></div>
