Metamath Proof Explorer


Theorem qdencl

Description: The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion qdencl ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 qnumdencl ( 𝐴 ∈ ℚ → ( ( numer ‘ 𝐴 ) ∈ ℤ ∧ ( denom ‘ 𝐴 ) ∈ ℕ ) )
2 1 simprd ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) ∈ ℕ )