theorem Crucial5X: :: MOEBIUS3:62

for n being Nat holds ln . ((Partial_Product Reci-seq2) . n) <= (Partial_Sums ReciPrime) . n