Theorem qsubcl

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

	Ref	Expression
Assertion	qsubcl	$$⊢\left(A\in \mathbb{Q}\wedge B\in \mathbb{Q}\right)\to A-B\in \mathbb{Q}$$

Proof

Step	Hyp	Ref	Expression
1		qcn	$$⊢A\in \mathbb{Q}\to A\in ℂ$$
2		qcn	$$⊢B\in \mathbb{Q}\to B\in ℂ$$
3		negsub	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+\left(-B\right)=A-B$$
4	1 2 3	syl2an	$$⊢\left(A\in \mathbb{Q}\wedge B\in \mathbb{Q}\right)\to A+\left(-B\right)=A-B$$
5		qnegcl	$$⊢B\in \mathbb{Q}\to -B\in \mathbb{Q}$$
6		qaddcl	$$⊢\left(A\in \mathbb{Q}\wedge -B\in \mathbb{Q}\right)\to A+\left(-B\right)\in \mathbb{Q}$$
7	5 6	sylan2	$$⊢\left(A\in \mathbb{Q}\wedge B\in \mathbb{Q}\right)\to A+\left(-B\right)\in \mathbb{Q}$$
8	4 7	eqeltrrd	$$⊢\left(A\in \mathbb{Q}\wedge B\in \mathbb{Q}\right)\to A-B\in \mathbb{Q}$$