theorem :: NUMBER10:22

primeindex 2 = 0 by Def4, MOEBIUS2:8;