set f = ReciPrime ;
for n, m being Nat st n < m holds
ReciPrime . m < ReciPrime . n
proof
let n, m be Nat; :: thesis: ( n < m implies ReciPrime . m < ReciPrime . n )
assume A1: n < m ; :: thesis: ReciPrime . m < ReciPrime . n
( ReciPrime . n = 1 / (primenumber n) & ReciPrime . m = 1 / (primenumber m) ) by ReciPr;
hence ReciPrime . m < ReciPrime . n by A1, Cosik1, XREAL_1:76; :: thesis: verum
end;
hence ReciPrime is decreasing by SEQM_3:4; :: thesis: ReciPrime is bounded_below
for n being Nat holds ReciPrime . n > 0
proof
let n be Nat; :: thesis: ReciPrime . n > 0
ReciPrime . n = 1 / (primenumber n) by ReciPr;
hence ReciPrime . n > 0 ; :: thesis: verum
end;
hence ReciPrime is bounded_below ; :: thesis: verum