Theorem mulclnq

Description: Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	mulclnq	|- ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) e. Q. )

Proof

Step	Hyp	Ref	Expression
1		mulpqnq	|- ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) = ( /Q ` ( A .pQ B ) ) )
2		elpqn	|- ( A e. Q. -> A e. ( N. X. N. ) )
3		elpqn	|- ( B e. Q. -> B e. ( N. X. N. ) )
4		mulpqf	|- .pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. )
5	4	fovcl	|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) e. ( N. X. N. ) )
6	2 3 5	syl2an	|- ( ( A e. Q. /\ B e. Q. ) -> ( A .pQ B ) e. ( N. X. N. ) )
7		nqercl	|- ( ( A .pQ B ) e. ( N. X. N. ) -> ( /Q ` ( A .pQ B ) ) e. Q. )
8	6 7	syl	|- ( ( A e. Q. /\ B e. Q. ) -> ( /Q ` ( A .pQ B ) ) e. Q. )
9	1 8	eqeltrd	|- ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) e. Q. )