theorem :: NUMBER10:24

primeindex 5 = 2 by Def4, MOEBIUS2:12;