Metamath Proof Explorer

Theorem xnegeq

Description: Equality of two extended numbers with -e in front of them. (Contributed by FL, 26-Dec-2011) (Proof shortened by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xnegeq ⊢ A = B → − A = − B

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ A = B → A = +∞ ↔ B = +∞
2 eqeq1 ⊢ A = B → A = −∞ ↔ B = −∞
3 negeq ⊢ A = B → − A = − B
4 2 3 ifbieq2d ⊢ A = B → if A = −∞ +∞ − A = if B = −∞ +∞ − B
5 1 4 ifbieq2d ⊢ A = B → if A = +∞ −∞ if A = −∞ +∞ − A = if B = +∞ −∞ if B = −∞ +∞ − B
6 df-xneg ⊢ − A = if A = +∞ −∞ if A = −∞ +∞ − A
7 df-xneg ⊢ − B = if B = +∞ −∞ if B = −∞ +∞ − B
8 5 6 7 3eqtr4g ⊢ A = B → − A = − B