MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xnegeq Structured version   Visualization version   GIF version

Theorem xnegeq 12035
Description: Equality of two extended numbers with -𝑒 in front of them. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xnegeq (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵)

Proof of Theorem xnegeq
StepHypRef Expression
1 eqeq1 2625 . . 3 (𝐴 = 𝐵 → (𝐴 = +∞ ↔ 𝐵 = +∞))
2 eqeq1 2625 . . . 4 (𝐴 = 𝐵 → (𝐴 = -∞ ↔ 𝐵 = -∞))
3 negeq 10270 . . . 4 (𝐴 = 𝐵 → -𝐴 = -𝐵)
42, 3ifbieq2d 4109 . . 3 (𝐴 = 𝐵 → if(𝐴 = -∞, +∞, -𝐴) = if(𝐵 = -∞, +∞, -𝐵))
51, 4ifbieq2d 4109 . 2 (𝐴 = 𝐵 → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵)))
6 df-xneg 11943 . 2 -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
7 df-xneg 11943 . 2 -𝑒𝐵 = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵))
85, 6, 73eqtr4g 2680 1 (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1482  ifcif 4084  +∞cpnf 10068  -∞cmnf 10069  -cneg 10264  -𝑒cxne 11940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rex 2917  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-iota 5849  df-fv 5894  df-ov 6650  df-neg 10266  df-xneg 11943
This theorem is referenced by:  xnegcl  12041  xnegneg  12042  xneg11  12043  xltnegi  12044  xnegid  12066  xnegdi  12075  xsubge0  12088  xlesubadd  12090  xmulneg1  12096  xmulneg2  12097  xmulmnf1  12103  xmulm1  12108  xrsdsval  19784  xrsdsreclblem  19786  xblss2ps  22200  xblss2  22201  xrhmeo  22739  xaddeq0  29503  xrsmulgzz  29663  xrge0npcan  29679  carsgclctunlem2  30366  xnegeqd  39483  xnegeqi  39486  supminfxr2  39518  supminfxrrnmpt  39520
  Copyright terms: Public domain W3C validator