Theorem resubcli

Description: Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997) (Revised by Mario Carneiro, 27-May-2016)

	Ref	Expression
Hypotheses	renegcl.1	$$⊢A\in ℝ$$
	resubcl.2	$$⊢B\in ℝ$$
Assertion	resubcli	$$⊢A-B\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		renegcl.1	$$⊢A\in ℝ$$
2		resubcl.2	$$⊢B\in ℝ$$
3	1	recni	$$⊢A\in ℂ$$
4	2	recni	$$⊢B\in ℂ$$
5		negsub	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+\left(-B\right)=A-B$$
6	3 4 5	mp2an	$$⊢A+\left(-B\right)=A-B$$
7	2	renegcli	$$⊢-B\in ℝ$$
8	1 7	readdcli	$$⊢A+\left(-B\right)\in ℝ$$
9	6 8	eqeltrri	$$⊢A-B\in ℝ$$