Theorem xnpcan

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

	Ref	Expression
Assertion	xnpcan	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rexr	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
2		xnegneg	⊢ ( 𝐵 ∈ ℝ* → -𝑒 -𝑒 𝐵 = 𝐵 )
3	1 2	syl	⊢ ( 𝐵 ∈ ℝ → -𝑒 -𝑒 𝐵 = 𝐵 )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → -𝑒 -𝑒 𝐵 = 𝐵 )
5	4	oveq2d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 -𝑒 -𝑒 𝐵 ) = ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) )
6		rexneg	⊢ ( 𝐵 ∈ ℝ → -𝑒 𝐵 = - 𝐵 )
7		renegcl	⊢ ( 𝐵 ∈ ℝ → - 𝐵 ∈ ℝ )
8	6 7	eqeltrd	⊢ ( 𝐵 ∈ ℝ → -𝑒 𝐵 ∈ ℝ )
9		xpncan	⊢ ( ( 𝐴 ∈ ℝ* ∧ -𝑒 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 -𝑒 -𝑒 𝐵 ) = 𝐴 )
10	8 9	sylan2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 -𝑒 -𝑒 𝐵 ) = 𝐴 )
11	5 10	eqtr3d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐴 )