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 
|- ( A e. QQ -> ( A x. ( denom ` A ) ) = ( numer ` A ) )

Proof

Step Hyp Ref Expression
1 qeqnumdivden 
 |-  ( A e. QQ -> A = ( ( numer ` A ) / ( denom ` A ) ) )
2 1 oveq1d 
 |-  ( A e. QQ -> ( A x. ( denom ` A ) ) = ( ( ( numer ` A ) / ( denom ` A ) ) x. ( denom ` A ) ) )
3 qnumcl 
 |-  ( A e. QQ -> ( numer ` A ) e. ZZ )
4 3 zcnd 
 |-  ( A e. QQ -> ( numer ` A ) e. CC )
5 qdencl 
 |-  ( A e. QQ -> ( denom ` A ) e. NN )
6 5 nncnd 
 |-  ( A e. QQ -> ( denom ` A ) e. CC )
7 5 nnne0d 
 |-  ( A e. QQ -> ( denom ` A ) =/= 0 )
8 4 6 7 divcan1d 
 |-  ( A e. QQ -> ( ( ( numer ` A ) / ( denom ` A ) ) x. ( denom ` A ) ) = ( numer ` A ) )
9 2 8 eqtrd 
 |-  ( A e. QQ -> ( A x. ( denom ` A ) ) = ( numer ` A ) )