Metamath Proof Explorer


Theorem recgt0i

Description: The reciprocal of a positive number is positive. Exercise 4 of Apostol p. 21. (Contributed by NM, 15-May-1999)

Ref Expression
Hypothesis ltplus1.1 A
Assertion recgt0i 0 < A 0 < 1 A

Proof

Step Hyp Ref Expression
1 ltplus1.1 A
2 recgt0 A 0 < A 0 < 1 A
3 1 2 mpan 0 < A 0 < 1 A