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