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 e. RR
Assertion recgt0i 
|- ( 0 < A -> 0 < ( 1 / A ) )

Proof

Step Hyp Ref Expression
1 ltplus1.1 
 |-  A e. RR
2 recgt0 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < ( 1 / A ) )
3 1 2 mpan 
 |-  ( 0 < A -> 0 < ( 1 / A ) )