for n being Nat holds 0 <= ReciPrime . n

proof

let n be Nat; :: thesis: 0 <= ReciPrime . n
ReciPrime . n in rng ReciPrime by FUNCT_2:4, ORDINAL1:def 12;
hence 0 <= ReciPrime . n by PARTFUN3:def 4; :: thesis: verum

end;

hence for b₁ being Real_Sequence st b₁ = Partial_Sums ReciPrime holds
b₁ is non-decreasing by SERIES_1:16; :: thesis: verum