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

Theorem xnegeq 12242
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 2774 . . 3 (𝐴 = 𝐵 → (𝐴 = +∞ ↔ 𝐵 = +∞))
2 eqeq1 2774 . . . 4 (𝐴 = 𝐵 → (𝐴 = -∞ ↔ 𝐵 = -∞))
3 negeq 10474 . . . 4 (𝐴 = 𝐵 → -𝐴 = -𝐵)
42, 3ifbieq2d 4248 . . 3 (𝐴 = 𝐵 → if(𝐴 = -∞, +∞, -𝐴) = if(𝐵 = -∞, +∞, -𝐵))
51, 4ifbieq2d 4248 . 2 (𝐴 = 𝐵 → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵)))
6 df-xneg 12150 . 2 -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
7 df-xneg 12150 . 2 -𝑒𝐵 = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵))
85, 6, 73eqtr4g 2829 1 (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  ifcif 4223  +∞cpnf 10272  -∞cmnf 10273  -cneg 10468  -𝑒cxne 12147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rex 3066  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-iota 5994  df-fv 6039  df-ov 6795  df-neg 10470  df-xneg 12150
This theorem is referenced by:  xnegcl  12248  xnegneg  12249  xneg11  12250  xltnegi  12251  xnegid  12273  xnegdi  12282  xsubge0  12295  xlesubadd  12297  xmulneg1  12303  xmulneg2  12304  xmulmnf1  12310  xmulm1  12315  xrsdsval  20004  xrsdsreclblem  20006  xblss2ps  22425  xblss2  22426  xrhmeo  22964  xaddeq0  29852  xrsmulgzz  30012  xrge0npcan  30028  carsgclctunlem2  30715  xnegeqd  40174  xnegeqi  40177  supminfxr2  40209  supminfxrrnmpt  40211
  Copyright terms: Public domain W3C validator