Add archpr to iset.mm
Add archpr to iset.mm

Unlike in set.mm, it doesn't seem we'll prove the Archimedean
property for RR from completeness, but instead prove it from
archnqq and up through the positive reals and so on. This commit
is the first step: the positive reals. And the proof is fairly
straightforward from archnqq and existing positive real theorems.
Most of the verbosity has to do with details such as
embedding N. into P.

metamath/set.mm,metamath/set.mm,metamath/set.mm