Theorem qmuldeneqnum

Description: Multiplying a rational by its denominator results in an integer. (Contributed by Stefan O'Rear, 13-Sep-2014)

	Ref	Expression
Assertion	qmuldeneqnum	⊢ ( 𝐴 ∈ ℚ → ( 𝐴 · ( denom ‘ 𝐴 ) ) = ( numer ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		qeqnumdivden	⊢ ( 𝐴 ∈ ℚ → 𝐴 = ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) )
2	1	oveq1d	⊢ ( 𝐴 ∈ ℚ → ( 𝐴 · ( denom ‘ 𝐴 ) ) = ( ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) · ( denom ‘ 𝐴 ) ) )
3		qnumcl	⊢ ( 𝐴 ∈ ℚ → ( numer ‘ 𝐴 ) ∈ ℤ )
4	3	zcnd	⊢ ( 𝐴 ∈ ℚ → ( numer ‘ 𝐴 ) ∈ ℂ )
5		qdencl	⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) ∈ ℕ )
6	5	nncnd	⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) ∈ ℂ )
7	5	nnne0d	⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) ≠ 0 )
8	4 6 7	divcan1d	⊢ ( 𝐴 ∈ ℚ → ( ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) · ( denom ‘ 𝐴 ) ) = ( numer ‘ 𝐴 ) )
9	2 8	eqtrd	⊢ ( 𝐴 ∈ ℚ → ( 𝐴 · ( denom ‘ 𝐴 ) ) = ( numer ‘ 𝐴 ) )