This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐴 )