Theorem qsubcl

Description: Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004)

	Ref	Expression
Assertion	qsubcl	|- ( ( A e. QQ /\ B e. QQ ) -> ( 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		negsub	|- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
4	1 2 3	syl2an	|- ( ( A e. QQ /\ B e. QQ ) -> ( A + -u B ) = ( A - B ) )
5		qnegcl	|- ( B e. QQ -> -u B e. QQ )
6		qaddcl	|- ( ( A e. QQ /\ -u B e. QQ ) -> ( A + -u B ) e. QQ )
7	5 6	sylan2	|- ( ( A e. QQ /\ B e. QQ ) -> ( A + -u B ) e. QQ )
8	4 7	eqeltrrd	|- ( ( A e. QQ /\ B e. QQ ) -> ( A - B ) e. QQ )