Theorem qdivcl

Description: Closure of division of rationals. (Contributed by NM, 3-Aug-2004)

	Ref	Expression
Assertion	qdivcl	|- ( ( A e. QQ /\ B e. QQ /\ B =/= 0 ) -> ( A / B ) e. QQ )

Proof

Step	Hyp	Ref	Expression
1		qcn	|- ( A e. QQ -> A e. CC )
2		qcn	|- ( B e. QQ -> B e. CC )
3		id	|- ( B =/= 0 -> B =/= 0 )
4		divrec	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
5	1 2 3 4	syl3an	|- ( ( A e. QQ /\ B e. QQ /\ B =/= 0 ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
6		qreccl	|- ( ( B e. QQ /\ B =/= 0 ) -> ( 1 / B ) e. QQ )
7		qmulcl	|- ( ( A e. QQ /\ ( 1 / B ) e. QQ ) -> ( A x. ( 1 / B ) ) e. QQ )
8	6 7	sylan2	|- ( ( A e. QQ /\ ( B e. QQ /\ B =/= 0 ) ) -> ( A x. ( 1 / B ) ) e. QQ )
9	8	3impb	|- ( ( A e. QQ /\ B e. QQ /\ B =/= 0 ) -> ( A x. ( 1 / B ) ) e. QQ )
10	5 9	eqeltrd	|- ( ( A e. QQ /\ B e. QQ /\ B =/= 0 ) -> ( A / B ) e. QQ )