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	⊢ ( ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) → ( numer ‘ 𝐴 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		qnumcl	⊢ ( 𝐴 ∈ ℚ → ( numer ‘ 𝐴 ) ∈ ℤ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) → ( numer ‘ 𝐴 ) ∈ ℤ )
3		qnumgt0	⊢ ( 𝐴 ∈ ℚ → ( 0 < 𝐴 ↔ 0 < ( numer ‘ 𝐴 ) ) )
4	3	biimpa	⊢ ( ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) → 0 < ( numer ‘ 𝐴 ) )
5		elnnz	⊢ ( ( numer ‘ 𝐴 ) ∈ ℕ ↔ ( ( numer ‘ 𝐴 ) ∈ ℤ ∧ 0 < ( numer ‘ 𝐴 ) ) )
6	2 4 5	sylanbrc	⊢ ( ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) → ( numer ‘ 𝐴 ) ∈ ℕ )