Theorem qgt0numnn

Description: A rational is positive iff its canonical numerator is a positive integer. (Contributed by Stefan O'Rear, 15-Sep-2014)

	Ref	Expression
Assertion	qgt0numnn	|- ( ( A e. QQ /\ 0 < A ) -> ( numer ` A ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		qnumcl	|- ( A e. QQ -> ( numer ` A ) e. ZZ )
2	1	adantr	|- ( ( A e. QQ /\ 0 < A ) -> ( numer ` A ) e. ZZ )
3		qnumgt0	|- ( A e. QQ -> ( 0 < A <-> 0 < ( numer ` A ) ) )
4	3	biimpa	|- ( ( A e. QQ /\ 0 < A ) -> 0 < ( numer ` A ) )
5		elnnz	|- ( ( numer ` A ) e. NN <-> ( ( numer ` A ) e. ZZ /\ 0 < ( numer ` A ) ) )
6	2 4 5	sylanbrc	|- ( ( A e. QQ /\ 0 < A ) -> ( numer ` A ) e. NN )