Theorem resubcl

Description: Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997)

	Ref	Expression
Assertion	resubcl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A-B\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢A\in ℝ\to A\in ℂ$$
2		recn	$$⊢B\in ℝ\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 ℝ\wedge B\in ℝ\right)\to A+\left(-B\right)=A-B$$
5		renegcl	$$⊢B\in ℝ\to -B\in ℝ$$
6		readdcl	$$⊢\left(A\in ℝ\wedge -B\in ℝ\right)\to A+\left(-B\right)\in ℝ$$
7	5 6	sylan2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+\left(-B\right)\in ℝ$$
8	4 7	eqeltrrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A-B\in ℝ$$