Description: The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | qdencl | ⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) ∈ ℕ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | qnumdencl | ⊢ ( 𝐴 ∈ ℚ → ( ( numer ‘ 𝐴 ) ∈ ℤ ∧ ( denom ‘ 𝐴 ) ∈ ℕ ) ) | |
2 | 1 | simprd | ⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) ∈ ℕ ) |