Description: The preimage of an unbounded below, open interval, with positive upper bound, for the reciprocal function. (Contributed by Glauco Siliprandi, 26-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pimrecltpos.x | |
|
pimrecltpos.b | |
||
pimrecltpos.n | |
||
pimrecltpos.c | |
||
Assertion | pimrecltpos | |