Theorem xnpcan

Description: Extended real version of npcan . (Contributed by Mario Carneiro, 20-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		rexr	$$⊢B\in ℝ\to B\in {ℝ}^{*}$$
2		xnegneg	$$⊢B\in {ℝ}^{*}\to -\left(-B\right)=B$$
3	1 2	syl	$$⊢B\in ℝ\to -\left(-B\right)=B$$
4	3	adantl	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\right)\to -\left(-B\right)=B$$
5	4	oveq2d	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\right)\to \left(A{+}_{𝑒}\left(-B\right)\right){+}_{𝑒}\left(-\left(-B\right)\right)=\left(A{+}_{𝑒}\left(-B\right)\right){+}_{𝑒}B$$
6		rexneg	$$⊢B\in ℝ\to -B=-B$$
7		renegcl	$$⊢B\in ℝ\to -B\in ℝ$$
8	6 7	eqeltrd	$$⊢B\in ℝ\to -B\in ℝ$$
9		xpncan	$$⊢\left(A\in {ℝ}^{*}\wedge -B\in ℝ\right)\to \left(A{+}_{𝑒}\left(-B\right)\right){+}_{𝑒}\left(-\left(-B\right)\right)=A$$
10	8 9	sylan2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\right)\to \left(A{+}_{𝑒}\left(-B\right)\right){+}_{𝑒}\left(-\left(-B\right)\right)=A$$
11	5 10	eqtr3d	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\right)\to \left(A{+}_{𝑒}\left(-B\right)\right){+}_{𝑒}B=A$$