resubcl

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

		Ref	Expression
	Assertion	resubcl	$⊢ (A \in ℝ \land B \in ℝ) \to A - B \in ℝ$

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		recn	$⊢ B \in ℝ \to B \in ℂ$
3		negsub	$⊢ (A \in ℂ \land B \in ℂ) \to A + (- B) = A - B$
4	1 2 3	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to A + (- B) = A - B$
5		renegcl	$⊢ B \in ℝ \to - B \in ℝ$
6		readdcl	$⊢ (A \in ℝ \land - B \in ℝ) \to A + (- B) \in ℝ$
7	5 6	sylan2	$⊢ (A \in ℝ \land B \in ℝ) \to A + (- B) \in ℝ$
8	4 7	eqeltrrd	$⊢ (A \in ℝ \land B \in ℝ) \to A - B \in ℝ$

Metamath Proof Explorer