This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐴 ) )