let n be Nat; :: thesis: ln . ((Partial_Product Reci-seq2) . (indexp n)) <= (Partial_Sums ReciPrime) . n
A1: ln . ((Partial_Product Reci-seq2) . (indexp n)) <= (Partial_Sums ReciPrime) . (indexp n) by Crucial5X;
for i being Nat holds ReciPrime . i >= 0
proof
let i be Nat; :: thesis: ReciPrime . i >= 0
ReciPrime . i = 1 / (primenumber i) by MOEBIUS2:def 1;
hence ReciPrime . i >= 0 ; :: thesis: verum
end;
then (Partial_Sums ReciPrime) . (indexp n) <= (Partial_Sums ReciPrime) . n by Krzys1, CATALAN2:52;
hence ln . ((Partial_Product Reci-seq2) . (indexp n)) <= (Partial_Sums ReciPrime) . n by A1, XXREAL_0:2; :: thesis: verum