Metamath Proof Explorer


Theorem xneg11

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

Ref Expression
Assertion xneg11 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( -𝑒 𝐴 = -𝑒 𝐵𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 xnegeq ( -𝑒 𝐴 = -𝑒 𝐵 → -𝑒 -𝑒 𝐴 = -𝑒 -𝑒 𝐵 )
2 xnegneg ( 𝐴 ∈ ℝ* → -𝑒 -𝑒 𝐴 = 𝐴 )
3 xnegneg ( 𝐵 ∈ ℝ* → -𝑒 -𝑒 𝐵 = 𝐵 )
4 2 3 eqeqan12d ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( -𝑒 -𝑒 𝐴 = -𝑒 -𝑒 𝐵𝐴 = 𝐵 ) )
5 1 4 syl5ib ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( -𝑒 𝐴 = -𝑒 𝐵𝐴 = 𝐵 ) )
6 xnegeq ( 𝐴 = 𝐵 → -𝑒 𝐴 = -𝑒 𝐵 )
7 5 6 impbid1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( -𝑒 𝐴 = -𝑒 𝐵𝐴 = 𝐵 ) )