theorem :: MOEBIUS2:24

lim ReciPrime = 0 by LimId, RecSub, SEQ_4:17;