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	⊢ 𝐴 ∈ ℝ
	resubcl.2	⊢ 𝐵 ∈ ℝ
Assertion	resubcli	⊢ ( 𝐴 − 𝐵 ) ∈ ℝ

Proof

Step	Hyp	Ref	Expression
1		renegcl.1	⊢ 𝐴 ∈ ℝ
2		resubcl.2	⊢ 𝐵 ∈ ℝ
3	1	recni	⊢ 𝐴 ∈ ℂ
4	2	recni	⊢ 𝐵 ∈ ℂ
5		negsub	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 ) )
6	3 4 5	mp2an	⊢ ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 )
7	2	renegcli	⊢ - 𝐵 ∈ ℝ
8	1 7	readdcli	⊢ ( 𝐴 + - 𝐵 ) ∈ ℝ
9	6 8	eqeltrri	⊢ ( 𝐴 − 𝐵 ) ∈ ℝ