Theorem rexsub

Description: Extended real subtraction when both arguments are real. (Contributed by Mario Carneiro, 23-Aug-2015)

	Ref	Expression
Assertion	rexsub	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A{+}_{𝑒}\left(-B\right)=A-B$$

Proof

Step	Hyp	Ref	Expression
1		rexneg	$$⊢B\in ℝ\to -B=-B$$
2	1	adantl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to -B=-B$$
3	2	oveq2d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A{+}_{𝑒}\left(-B\right)=A{+}_{𝑒}\left(-B\right)$$
4		renegcl	$$⊢B\in ℝ\to -B\in ℝ$$
5		rexadd	$$⊢\left(A\in ℝ\wedge -B\in ℝ\right)\to A{+}_{𝑒}\left(-B\right)=A+\left(-B\right)$$
6	4 5	sylan2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A{+}_{𝑒}\left(-B\right)=A+\left(-B\right)$$
7		recn	$$⊢A\in ℝ\to A\in ℂ$$
8		recn	$$⊢B\in ℝ\to B\in ℂ$$
9		negsub	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+\left(-B\right)=A-B$$
10	7 8 9	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+\left(-B\right)=A-B$$
11	3 6 10	3eqtrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A{+}_{𝑒}\left(-B\right)=A-B$$