theorem :: NUMBER10:25

primeindex 7 = 3 by Def4, MOEBIUS2:15;