ACL2(r) recognizer for infinitely large numbers

(I-large x) is true if and only if x is non-zero and 1/x is an infinitesimal number. This predicate is only defined in ACL2(r) (see real).