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 ⊢ A ∈ ℝ * ∧ B ∈ ℝ → A + 𝑒 − B + 𝑒 B = A

Proof

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