theorem :: NUMBER10:23

primeindex 3 = 1 by Def4, MOEBIUS2:10;