theorem :: NUMBER10:27

primeindex 13 = 5 by Def4, MOEBIUS2:19;